********************************************************
Schubert's Steamroller.

(define schubert
  {--> symbol}
   -> (kb-> [ [all x [[wolf x] => [animal x]]]
        [all x [[fox x] => [animal x]]]
        [all x [[bird x] => [animal x]]]
        [all x [[caterpillar x] => [animal x]]]
        [all x [[snail x] => [animal x]]]
        [all x [[grain x] => [plant x]]]
        
        [exists x [wolf x]]
        [exists x [fox x]]
        [exists x [bird x]]
        [exists x [caterpillar x]]
        [exists x [snail x]]
        [exists x [grain x]]
        
        [all x [[animal x] => [[all y [[plant y] => [eats x y]]]
                    v 
                    [all z [[[[animal z] &
                             [smaller z x]] &
                             [exists u [[plant u] & [eats z u]]]]
                             => 
                             [eats x z]]]]]]

        [all x [all y [[[caterpillar x] & [bird y]] => [smaller x y]]]]
        [all x [all y [[[snail x] & [bird y]]  =>  [smaller x y]]]]
        [all x [all y [[[bird x] & [fox y]]  =>  [smaller x y]]]]
        [all x [all y [[[fox x] & [wolf y]]  =>  [smaller x y]]]]
        [all x [all y [[[bird x] & [caterpillar y]]  =>  [eats x y]]]]
        
        [all x [[caterpillar x]  
                 =>  [exists y [[plant y] & [eats x y]]]]]
        [all x [[snail x]        
                 =>  [exists y [[plant y] & [eats x y]]]]]

        [all x [all y [[[wolf x] & [fox y]]  =>  [~ [eats x y]]]]]
        [all x [all y [[[wolf x] & [grain y]]  =>  [~ [eats x y]]]]]
        [all x [all y [[[bird x] & [snail y]]  =>  [~ [eats x y]]]]] ]))
                     
(schubert)  

(define steamroller
  {--> prop}
   -> [exists x [exists y [[[animal x] &
	                       [animal y]] &
	                         [[eats x y] &
                              [all z [[grain z] => [eats y z]]]]]]])

(<-kb (steamroller))                              
run time: 0.984375 secs
5088693 inferences, equality = false
depth = 20, complexity = -1, timeout = 60 secs
true
******************************************************
Step 1

? (exists x (exists y (((animal x) & (animal y)) & ((eats x y) & (all z ((grain z) => (eats y z)))))))


> revsk
=============================
Step 2

? (exists x45052 (exists x45053 (((animal x45052) & (animal x45053)) & ((eats x45052 x45053) & ((~ (grain (f45055 x45052 x45053))) v (eats x45053 (f45055 x45052 x45053)))))))


> eR
=============================
Step 3

? (exists x45053 (((animal Var188) & (animal x45053)) & ((eats Var188 x45053) & ((~ (grain (f45055 Var188 x45053))) v (eats x45053 (f45055 Var188 x45053))))))


> eR
=============================
Step 4

? (((animal Var188) & (animal Var190)) & ((eats Var188 Var190) & ((~ (grain (f45055 Var188 Var190))) v (eats Var190 (f45055 Var188 Var190)))))


> &r
|=============================
|Step 5
|
|? ((animal Var188) & (animal Var190))
|
|
|> &r
||=============================
||Step 6
||
||? (animal c40924)
||
||
||> hypdisj
||=============================
||Step 7
||
||? (animal c40924)
||
||
||> ((animal X) <-- (fox X))
||=============================
||Step 8
||
||? (fox c40924)
||
||1. (~ (animal c40924))
||
||> ((fox c40924) <--)
|=============================
|Step 9
|
|? (animal c40922)
|
|
|> hypdisj
|=============================
|Step 10
|
|? (animal c40922)
|
|
|> ((animal X) <-- (bird X))
|=============================
|Step 11
|
|? (bird c40922)
|
|1. (~ (animal c40922))
|
|> ((bird c40922) <--)
=============================
Step 12

? ((eats c40924 c40922) & ((~ (grain (f45055 c40924 c40922))) v (eats c40922 (f45055 c40924 c40922))))


> &r
|=============================
|Step 13
|
|? (eats c40924 c40922)
|
|
|> hypdisj
|=============================
|Step 14
|
|? (eats c40924 c40922)
|
|
|> ((eats Y Z) <-- (animal Y) (plant X) (~ (eats Y X)) (animal Z) (smaller Z Y) (plant W) (eats Z W))
|||||||=============================
|||||||Step 15
|||||||
|||||||? (animal c40924)
|||||||
|||||||1. (~ (eats c40924 c40922))
|||||||
|||||||> ((animal X) <-- (fox X))
|||||||=============================
|||||||Step 16
|||||||
|||||||? (fox c40924)
|||||||
|||||||1. (~ (animal c40924))
|||||||2. (~ (eats c40924 c40922))
|||||||
|||||||> ((fox c40924) <--)
||||||=============================
||||||Step 17
||||||
||||||? (plant Var215)
||||||
||||||1. (~ (eats c40924 c40922))
||||||
||||||> ((plant X) <-- (grain X))
||||||=============================
||||||Step 18
||||||
||||||? (grain c40916)
||||||
||||||1. (~ (plant c40916))
||||||2. (~ (eats c40924 c40922))
||||||
||||||> ((grain c40916) <--)
|||||=============================
|||||Step 19
|||||
|||||? (~ (eats c40924 c40916))
|||||
|||||1. (~ (eats c40924 c40922))
|||||
|||||> ((~ (eats W Y)) <-- (animal Z) (plant X) (~ (eats Z X)) (animal W) (smaller W Z) (plant Y) (~ (eats Z W)))
|||||||||||=============================
|||||||||||Step 20
|||||||||||
|||||||||||? (animal Var228)
|||||||||||
|||||||||||1. (eats c40924 c40916)
|||||||||||2. (~ (eats c40924 c40922))
|||||||||||
|||||||||||> ((animal X) <-- (wolf X))
|||||||||||=============================
|||||||||||Step 21
|||||||||||
|||||||||||? (wolf c40926)
|||||||||||
|||||||||||1. (~ (animal c40926))
|||||||||||2. (eats c40924 c40916)
|||||||||||3. (~ (eats c40924 c40922))
|||||||||||
|||||||||||> ((wolf c40926) <--)
||||||||||=============================
||||||||||Step 22
||||||||||
||||||||||? (plant Var227)
||||||||||
||||||||||1. (eats c40924 c40916)
||||||||||2. (~ (eats c40924 c40922))
||||||||||
||||||||||> ((plant X) <-- (grain X))
||||||||||=============================
||||||||||Step 23
||||||||||
||||||||||? (grain c40916)
||||||||||
||||||||||1. (~ (plant c40916))
||||||||||2. (eats c40924 c40916)
||||||||||3. (~ (eats c40924 c40922))
||||||||||
||||||||||> ((grain c40916) <--)
|||||||||=============================
|||||||||Step 24
|||||||||
|||||||||? (~ (eats c40926 c40916))
|||||||||
|||||||||1. (eats c40924 c40916)
|||||||||2. (~ (eats c40924 c40922))
|||||||||
|||||||||> ((~ (eats X Y)) <-- (wolf X) (grain Y))
||||||||||=============================
||||||||||Step 25
||||||||||
||||||||||? (wolf c40926)
||||||||||
||||||||||1. (eats c40926 c40916)
||||||||||2. (eats c40924 c40916)
||||||||||3. (~ (eats c40924 c40922))
||||||||||
||||||||||> ((wolf c40926) <--)
|||||||||=============================
|||||||||Step 26
|||||||||
|||||||||? (grain c40916)
|||||||||
|||||||||1. (eats c40926 c40916)
|||||||||2. (eats c40924 c40916)
|||||||||3. (~ (eats c40924 c40922))
|||||||||
|||||||||> ((grain c40916) <--)
||||||||=============================
||||||||Step 27
||||||||
||||||||? (animal c40924)
||||||||
||||||||1. (eats c40924 c40916)
||||||||2. (~ (eats c40924 c40922))
||||||||
||||||||> ((animal X) <-- (fox X))
||||||||=============================
||||||||Step 28
||||||||
||||||||? (fox c40924)
||||||||
||||||||1. (~ (animal c40924))
||||||||2. (eats c40924 c40916)
||||||||3. (~ (eats c40924 c40922))
||||||||
||||||||> ((fox c40924) <--)
|||||||=============================
|||||||Step 29
|||||||
|||||||? (smaller c40924 c40926)
|||||||
|||||||1. (eats c40924 c40916)
|||||||2. (~ (eats c40924 c40922))
|||||||
|||||||> ((smaller X Y) <-- (fox X) (wolf Y))
||||||||=============================
||||||||Step 30
||||||||
||||||||? (fox c40924)
||||||||
||||||||1. (~ (smaller c40924 c40926))
||||||||2. (eats c40924 c40916)
||||||||3. (~ (eats c40924 c40922))
||||||||
||||||||> ((fox c40924) <--)
|||||||=============================
|||||||Step 31
|||||||
|||||||? (wolf c40926)
|||||||
|||||||1. (~ (smaller c40924 c40926))
|||||||2. (eats c40924 c40916)
|||||||3. (~ (eats c40924 c40922))
|||||||
|||||||> ((wolf c40926) <--)
||||||=============================
||||||Step 32
||||||
||||||? (plant c40916)
||||||
||||||1. (eats c40924 c40916)
||||||2. (~ (eats c40924 c40922))
||||||
||||||> ((plant X) <-- (grain X))
||||||=============================
||||||Step 33
||||||
||||||? (grain c40916)
||||||
||||||1. (~ (plant c40916))
||||||2. (eats c40924 c40916)
||||||3. (~ (eats c40924 c40922))
||||||
||||||> ((grain c40916) <--)
|||||=============================
|||||Step 34
|||||
|||||? (~ (eats c40926 c40924))
|||||
|||||1. (eats c40924 c40916)
|||||2. (~ (eats c40924 c40922))
|||||
|||||> ((~ (eats X Y)) <-- (wolf X) (fox Y))
||||||=============================
||||||Step 35
||||||
||||||? (wolf c40926)
||||||
||||||1. (eats c40926 c40924)
||||||2. (eats c40924 c40916)
||||||3. (~ (eats c40924 c40922))
||||||
||||||> ((wolf c40926) <--)
|||||=============================
|||||Step 36
|||||
|||||? (fox c40924)
|||||
|||||1. (eats c40926 c40924)
|||||2. (eats c40924 c40916)
|||||3. (~ (eats c40924 c40922))
|||||
|||||> ((fox c40924) <--)
||||=============================
||||Step 37
||||
||||? (animal c40922)
||||
||||1. (~ (eats c40924 c40922))
||||
||||> ((animal X) <-- (bird X))
||||=============================
||||Step 38
||||
||||? (bird c40922)
||||
||||1. (~ (animal c40922))
||||2. (~ (eats c40924 c40922))
||||
||||> ((bird c40922) <--)
|||=============================
|||Step 39
|||
|||? (smaller c40922 c40924)
|||
|||1. (~ (eats c40924 c40922))
|||
|||> ((smaller X Y) <-- (bird X) (fox Y))
||||=============================
||||Step 40
||||
||||? (bird c40922)
||||
||||1. (~ (smaller c40922 c40924))
||||2. (~ (eats c40924 c40922))
||||
||||> ((bird c40922) <--)
|||=============================
|||Step 41
|||
|||? (fox c40924)
|||
|||1. (~ (smaller c40922 c40924))
|||2. (~ (eats c40924 c40922))
|||
|||> ((fox c40924) <--)
||=============================
||Step 42
||
||? (plant Var216)
||
||1. (~ (eats c40924 c40922))
||
||> ((plant X) <-- (grain X))
||=============================
||Step 43
||
||? (grain c40916)
||
||1. (~ (plant c40916))
||2. (~ (eats c40924 c40922))
||
||> ((grain c40916) <--)
|=============================
|Step 44
|
|? (eats c40922 c40916)
|
|1. (~ (eats c40924 c40922))
|
|> ((eats Z X) <-- (animal Z) (plant X) (animal W) (smaller W Z) (plant Y) (eats W Y) (~ (eats Z W)))
|||||||=============================
|||||||Step 45
|||||||
|||||||? (animal c40922)
|||||||
|||||||1. (~ (eats c40922 c40916))
|||||||2. (~ (eats c40924 c40922))
|||||||
|||||||> ((animal X) <-- (bird X))
|||||||=============================
|||||||Step 46
|||||||
|||||||? (bird c40922)
|||||||
|||||||1. (~ (animal c40922))
|||||||2. (~ (eats c40922 c40916))
|||||||3. (~ (eats c40924 c40922))
|||||||
|||||||> ((bird c40922) <--)
||||||=============================
||||||Step 47
||||||
||||||? (plant c40916)
||||||
||||||1. (~ (eats c40922 c40916))
||||||2. (~ (eats c40924 c40922))
||||||
||||||> ((plant X) <-- (grain X))
||||||=============================
||||||Step 48
||||||
||||||? (grain c40916)
||||||
||||||1. (~ (plant c40916))
||||||2. (~ (eats c40922 c40916))
||||||3. (~ (eats c40924 c40922))
||||||
||||||> ((grain c40916) <--)
|||||=============================
|||||Step 49
|||||
|||||? (animal Var280)
|||||
|||||1. (~ (eats c40922 c40916))
|||||2. (~ (eats c40924 c40922))
|||||
|||||> ((animal X) <-- (snail X))
|||||=============================
|||||Step 50
|||||
|||||? (snail c40918)
|||||
|||||1. (~ (animal c40918))
|||||2. (~ (eats c40922 c40916))
|||||3. (~ (eats c40924 c40922))
|||||
|||||> ((snail c40918) <--)
||||=============================
||||Step 51
||||
||||? (smaller c40918 c40922)
||||
||||1. (~ (eats c40922 c40916))
||||2. (~ (eats c40924 c40922))
||||
||||> ((smaller X Y) <-- (snail X) (bird Y))
|||||=============================
|||||Step 52
|||||
|||||? (snail c40918)
|||||
|||||1. (~ (smaller c40918 c40922))
|||||2. (~ (eats c40922 c40916))
|||||3. (~ (eats c40924 c40922))
|||||
|||||> ((snail c40918) <--)
||||=============================
||||Step 53
||||
||||? (bird c40922)
||||
||||1. (~ (smaller c40918 c40922))
||||2. (~ (eats c40922 c40916))
||||3. (~ (eats c40924 c40922))
||||
||||> ((bird c40922) <--)
|||=============================
|||Step 54
|||
|||? (plant (f40881 Var301))
|||
|||1. (~ (eats c40922 c40916))
|||2. (~ (eats c40924 c40922))
|||
|||> ((plant (f40881 X)) <-- (snail X))
|||=============================
|||Step 55
|||
|||? (snail c40918)
|||
|||1. (~ (plant (f40881 c40918)))
|||2. (~ (eats c40922 c40916))
|||3. (~ (eats c40924 c40922))
|||
|||> ((snail c40918) <--)
||=============================
||Step 56
||
||? (eats c40918 (f40881 c40918))
||
||1. (~ (eats c40922 c40916))
||2. (~ (eats c40924 c40922))
||
||> ((eats X (f40881 X)) <-- (snail X))
||=============================
||Step 57
||
||? (snail c40918)
||
||1. (~ (eats c40918 (f40881 c40918)))
||2. (~ (eats c40922 c40916))
||3. (~ (eats c40924 c40922))
||
||> ((snail c40918) <--)
|=============================
|Step 58
|
|? (~ (eats c40922 c40918))
|
|1. (~ (eats c40922 c40916))
|2. (~ (eats c40924 c40922))
|
|> ((~ (eats X Y)) <-- (bird X) (snail Y))
||=============================
||Step 59
||
||? (bird c40922)
||
||1. (eats c40922 c40918)
||2. (~ (eats c40922 c40916))
||3. (~ (eats c40924 c40922))
||
||> ((bird c40922) <--)
|=============================
|Step 60
|
|? (snail c40918)
|
|1. (eats c40922 c40918)
|2. (~ (eats c40922 c40916))
|3. (~ (eats c40924 c40922))
|
|> ((snail c40918) <--)
=============================
Step 61

? ((~ (grain (f45055 c40924 c40922))) v (eats c40922 (f45055 c40924 c40922)))


> hypdisj
=============================
Step 62

? (eats c40922 (f45055 c40924 c40922))

1. (grain (f45055 c40924 c40922))

> ((eats Z X) <-- (animal Z) (plant X) (animal W) (smaller W Z) (plant Y) (eats W Y) (~ (eats Z W)))
||||||=============================
||||||Step 63
||||||
||||||? (animal c40922)
||||||
||||||1. (~ (eats c40922 (f45055 c40924 c40922)))
||||||2. (grain (f45055 c40924 c40922))
||||||
||||||> ((animal X) <-- (bird X))
||||||=============================
||||||Step 64
||||||
||||||? (bird c40922)
||||||
||||||1. (~ (animal c40922))
||||||2. (~ (eats c40922 (f45055 c40924 c40922)))
||||||3. (grain (f45055 c40924 c40922))
||||||
||||||> ((bird c40922) <--)
|||||=============================
|||||Step 65
|||||
|||||? (plant (f45055 c40924 c40922))
|||||
|||||1. (~ (eats c40922 (f45055 c40924 c40922)))
|||||2. (grain (f45055 c40924 c40922))
|||||
|||||> ((plant X) <-- (grain X))
|||||=============================
|||||Step 66
|||||
|||||? (grain (f45055 c40924 c40922))
|||||
|||||1. (~ (plant (f45055 c40924 c40922)))
|||||2. (~ (eats c40922 (f45055 c40924 c40922)))
|||||3. (grain (f45055 c40924 c40922))
|||||
|||||> hyp
||||=============================
||||Step 67
||||
||||? (animal Var321)
||||
||||1. (~ (eats c40922 (f45055 c40924 c40922)))
||||2. (grain (f45055 c40924 c40922))
||||
||||> ((animal X) <-- (snail X))
||||=============================
||||Step 68
||||
||||? (snail c40918)
||||
||||1. (~ (animal c40918))
||||2. (~ (eats c40922 (f45055 c40924 c40922)))
||||3. (grain (f45055 c40924 c40922))
||||
||||> ((snail c40918) <--)
|||=============================
|||Step 69
|||
|||? (smaller c40918 c40922)
|||
|||1. (~ (eats c40922 (f45055 c40924 c40922)))
|||2. (grain (f45055 c40924 c40922))
|||
|||> ((smaller X Y) <-- (snail X) (bird Y))
||||=============================
||||Step 70
||||
||||? (snail c40918)
||||
||||1. (~ (smaller c40918 c40922))
||||2. (~ (eats c40922 (f45055 c40924 c40922)))
||||3. (grain (f45055 c40924 c40922))
||||
||||> ((snail c40918) <--)
|||=============================
|||Step 71
|||
|||? (bird c40922)
|||
|||1. (~ (smaller c40918 c40922))
|||2. (~ (eats c40922 (f45055 c40924 c40922)))
|||3. (grain (f45055 c40924 c40922))
|||
|||> ((bird c40922) <--)
||=============================
||Step 72
||
||? (plant (f40881 Var341))
||
||1. (~ (eats c40922 (f45055 c40924 c40922)))
||2. (grain (f45055 c40924 c40922))
||
||> ((plant (f40881 X)) <-- (snail X))
||=============================
||Step 73
||
||? (snail c40918)
||
||1. (~ (plant (f40881 c40918)))
||2. (~ (eats c40922 (f45055 c40924 c40922)))
||3. (grain (f45055 c40924 c40922))
||
||> ((snail c40918) <--)
|=============================
|Step 74
|
|? (eats c40918 (f40881 c40918))
|
|1. (~ (eats c40922 (f45055 c40924 c40922)))
|2. (grain (f45055 c40924 c40922))
|
|> ((eats X (f40881 X)) <-- (snail X))
|=============================
|Step 75
|
|? (snail c40918)
|
|1. (~ (eats c40918 (f40881 c40918)))
|2. (~ (eats c40922 (f45055 c40924 c40922)))
|3. (grain (f45055 c40924 c40922))
|
|> ((snail c40918) <--)
=============================
Step 76

? (~ (eats c40922 c40918))

1. (~ (eats c40922 (f45055 c40924 c40922)))
2. (grain (f45055 c40924 c40922))

> ((~ (eats X Y)) <-- (bird X) (snail Y))
|=============================
|Step 77
|
|? (bird c40922)
|
|1. (eats c40922 c40918)
|2. (~ (eats c40922 (f45055 c40924 c40922)))
|3. (grain (f45055 c40924 c40922))
|
|> ((bird c40922) <--)
=============================
Step 78

? (snail c40918)

1. (eats c40922 c40918)
2. (~ (eats c40922 (f45055 c40924 c40922)))
3. (grain (f45055 c40924 c40922))

> ((snail c40918) <--)
